(*
  Purpose: Simplification of Arithmetic Expressions.
  Author: Gang Chen
  Date:  Feb. 12, 2008
*)

Require Export Arith.
Require Import Omega.
Require Import base.

(** Arithmetic Simplification *)
Section ArithSimp.

(* move S out. *)
Lemma plus_SR : forall n m, n + S m = S (n+m).
Proof.
  auto with arith.
Qed.

Lemma plus_SL : forall n m, S n + m = S (n+m).
Proof.
  auto with arith.
Qed.

Lemma large_plus : 
  forall t0 t, t>t0 -> exists t1, t=(S t0)+t1.
Proof.
  intros.
  exists (t - (S t0)).
  auto with arith.
Qed.

Lemma small_plus : 
  forall t0 t, t0<t -> exists t1, t=(S t0)+t1.
Proof.
  intros.
  exists (t - (S t0)).
  auto with arith.
Qed.

(* equivalence between P(S(t0+t)) and t>t0 -> P(t). *)
Lemma plus_imply_large :
  forall (P : nat->Prop) t0, 
    (forall t, P (S (t0+t))) -> 
       (forall t, t0<t -> P t).
Proof.
  intros.
  assert (exists t1 : _, t = S (t0 + t1)).
  exists (t - t0 - 1).
  omega.
  elim H1.
  intro.
  intro.
  rewrite H2 in |- *.
  apply H.
Qed.

Lemma large_imply_plus :
  forall (P : nat->Prop) t0, 
    (forall t, t>t0 -> P t) -> (forall t, P (S (t0+t))).
Proof.
  intros; apply (H (S (t0+t))); auto with arith.
Qed.

Lemma plus_imply_less :
  forall (P : nat->Prop) t0 t1, 
    (forall t, t<t1-t0 -> P (S (t0+t))) -> 
       (forall t, t0<t /\ t<=t1 -> P t).
Proof.
  intros.
  assert (exists t1 : _, t = S (t0 + t1)).
  exists (t - t0 - 1).
  omega.
  elim H1.
  intro.
  intro.
  rewrite H2 in |- *.
  apply H.
  omega.
Qed.

Lemma imply_plus :
  forall (P : nat->Prop) t0 t1, 
    (forall t : nat, t < t1 -> P (t0 + t)) ->
    (forall t : nat, t0 < t < t0+t1 -> P t).
Proof.
intros.
assert (exists t' : _, t = t0 + t').
 exists (t - t0).
    omega.
elim H1.
  intros.
  rewrite H2 in |- *.
  apply H.
  rewrite H2 in H0.
  omega.
Qed.


Lemma imply_close_close :
  forall (P : nat->Prop) t0 d, 
    (forall t : nat, t <= d -> P (t0 + t)) ->
    (forall t : nat, close_close t0 t (t0+d) -> P t).
Proof.
  unfold close_close; intros.
  assert (exists t1 : _, t = t0 + t1).
  exists (t - t0).
  omega.
  elim H1.
  intro; intro.
  rewrite H2 in |- *.
  apply H.
   omega.
Qed.


End ArithSimp.
Hint Rewrite plus_0_l plus_0_r plus_SR plus_SL : arith_simp.
